perm filename RED.LM4[LSP,JRA]3 blob
sn#225087 filedate 1976-07-13 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 Corresponding to each of the three cases in the syntax of terms, there is
C00011 ENDMK
C⊗;
Corresponding to each of the three cases in the syntax of terms, there is
one semantic clause in the definition, by structural induction, of πV:
.begin indent 10,10;
1) Identifiers: given an environment πr, the value of an identifier ?x is
found by looking up its denotation in πr, that is, by applying πr to ?x:
.begin center;
$V?x|(πr) = πr%f(%1?x|⊗↓We use emphatic brackets "%f(%1" and "|" to enclose
terms of the ?λ-calculus.←
.end
2) Combinations, ∪MN∩: given πr the value of the rator ?M can be interpreted
as a function from $D to $D by application of $f, and this function can then
be meaningfully applied to the value of the rand ?N:
.begin center;
$V∪MN∩|(πr) = $f($V?M|(πr))($V?N|(πr))
.end
3) Abstractions: given πr, an abstraction ∪λx.M∩ is naturally interpreted as
a function from $D to $D. When applied to any argument πd from $D, the result
of this function is the value of the body ?M in an environment πr' identical
to πr in all respects, except that the bound variable ?x is now associated
with the argument πd. We write πr[πd/?x] for this %3⊗→extended environment↔←%1
πr' given by
.begin nofill;
πd if ?x'≡?x
πr'%f(%1?x'| =
πr%f(?x'| if ?x'%d≥%1?x
.end
As πd varies over $D, $V?M|(πr[πd/?x])⊗↓Note the difference between the
notations πr[πd/?x], and [∪d∩/?x]?M. In the first we get the extended
environment where πd is substituted for the value of ?x. In [∪d∩/?x]?M,
we get the expression ?M with all free occurrences of ?x itself replaced
by ∪d∩.← determines a continuous function, which is rendered as an element
of $D by application of $y, thus
.R17:
.begin center;
$V∪λx.M∩|(πr) = $y(?λπdε$D.$V?M|(πr[πd/?x]))⊗↓In "?λπdε$D." we are restricting
the argument πd just to the domain $D. We use this convention informally
in this section, we will make the concept of typed ?λ-notation
more precise in the next section, LCF.←
.end
.end
To establish that this interpretation of terms provides a model for the ?λ-calculus,
we must say how to interpret equations between terms in $D and show that
the axioms about equality of terms, in particular the conversion rules,
are true under this interpretation. We define two terms ?M and ?N to be
%3⊗→semantically equivalent↔←%1, or %3⊗→equal in %dD%4∞%1↔←, if they have the same value
in $D for all associations of values with their free variables:
.begin center;
?M $= ?N iff $V?M|(πr) = $V?N|(πr) for all πr
.end
That ⊗→%d=%4D∞%1↔← is a substitutive equivalence relation is straightforward from the
corresponding property of lattice equality in $D. To prove the validity of
the conversion rules, since they are defined in terms of substitution, we
need a lemma relating substitution and extended environments. First,
however, we list some obvious properties of environments.
%7LEMMA 5%1 For all πrε$N, πd, πd'ε$D, ?x, ?x'ε$I, and ?Mε$X,
.begin nofill;
a) ?x'≡?x => πr[πd/?x][πd'/?x'] = πr[πd'/?x']
b) ?x'∪≥∩?x => πr[πd/?x][πd'/?x'] = πr[πd'/?x'][πd/?x]
c) if ?x%5N%1∪FV(M)∩, then
i) $V?M|(πr[πd/?x]) = $V?M|(πr)
ii) $V?M|(πr[πd/?x][πd'/?x']) = $V?M|(πr[πd'/?x'])
.end
The next lemma says that extending environments correctly interprets substitution.
%7LEMMA 6%1 (The ⊗→substitution lemma↔←)####For all ∪M,N∩ε$X, ?xε$I, and πrε$N
.begin center;
$V[?N/?x]?M|(πr) = $V?M|(πr[$V?N|(πr)/?x])
.end
The proof of this lemma is not difficult, but it is very long and tedious, and
is omitted here. One may find it in Wadsworth [15]. Now we are ready to prove
that the conversion rules are valid in $D.
.group;
%7THEOREM 7%1
.begin tabit1(27);
\(?α) ∪λx.M∩ $= ∪λy.[y/x]M∩, provided ∪y≤FV(M)∩
\(?β) ∪(λx.M)N $= ∪[N/x]M∩
\(?h) ∪λx.Mx $= ?M, provided ∪x≤FV(M)∩
.end
.apart
.begin tabit2 (10,40); nofill;
.group
Proof:
\(?α) $V∪λy.[y/x]M∩|(πr) = $y(?λπdε$D.$V∪[y/x]M∩|(πr[πd/?y]))\
\\by 3) of the definition of πV
\ = $y(?λπdε$D.$V?M|(πr[πd/?y][$V?y|(πr[πd/?y])/?x]))
\\by Lemma 6
\ = $y(?λπdε$D.$V?M|(πr[πd/?y][πd/?x]))
\\by 1) of the definition of πV
\ = $y(?λπdε$D.$V?M|(πr[πd/?x]))
\\by Lemma 5 c)ii), since ∪y≤FV(M)∩
\ = $V∪λx.M∩|(πr)\by 3) of definition of πV
.apart
.group
\(?β) $V∪(λx.M)N∩|(πr) = $f($y(?λπdε$D.$V?M|(πr[πd/?x])))($V?N|(πr))
\\by 2) and 3) of definition of πV
\ = (?λπdε$D.$V?M|(πr[πd/?x]))($V?N|(πr))
\\since $f($y(πf)) = πf
\ = $V?M|(πr[$V?N|(πr)/?x])\by function application in
\\####the domain
\ = $V∪[N/x]M∩|(πr)\by the substitution lemma
.apart
.group
.begin indent 10,12;fill;
(?h) Note first that, for πfε[$D →$D], for all πdε$D,
(?λπdε$D.πf(πd))(πd) = πf(πd)
by the definition of the typed ?λ-notation;
so, by definition of equality in the function space [$D→$D]:
.end
.begin center;
(*) (?λπdε$D.πf(πd)) = πf, for all πfε[$D → $D]
.end
.apart;
.group;
\Then,
\$V∪λx.Mx∩|(πr) = $y(?λπdε$D.$V?M?x|(πr[πd/?x]))
\\ by 3) of definition of πV
\ = $y(?λπdε$D.$f($V?M|(πr[πd/?x]))($V?x|(πr[πd/?x])))
\\by 2) of definition of πV
\ = $y(?λπdε$D.$f($V?M|(πr))(πd))
\\since ∪x≤FV(M)∩ and by 1) of definition of πV
\ = $y($f($V?M|(πr)))\by (*) with πf ≡ $f($V?M|(πr))
\ = $V?M|(πr)\since $y($f(πx)) = πx
.end
.group
%7THEOREM 8%1 The interpretation defined by πV and the relation $=, constitutes
a model for the ?λ-calculus system based on ∪αβ∩?h-conversion:
.begin center;
∪M αβ?h-$c ?N => ?M $= ?N
.end
###########The proof is just a combination of the results from Lemmas 5 and 6, and Theorem 7.
.apart